Inference at * 1 2 
Iof proof for Lemma last-not-before:

.....antecedent..... NILNIL

1. T : Type
2. L : T List
3. (null(L))
4. no_repeats(T;L)
5. x : T
6. last(L) before x  L
7. x, y:T. x before y  L  ((x = y))
8. (last(L) = x)
  (x = last(L)) 

latex

 by ParallelOp (-1) 

latex

 .

Definitions	x:A. B(x), x:AB(x), x before y  l, no_repeats(T;l), type List, Type, t  T, , s = t, A, P  Q, False
Lemmas	not wf, false wf